A, B:Type, f:(A(B + Top)), ds:(IdType), da:(IdKndType), X:Interface(ds;da;A).
interface-compose(f;X)  Interface(ds;da;B) 

latex

Definitions	Interface(ds;da;A), interface-compose(f;X), g o f, x. t(x), x,y. t(x;y), x:A.B(x), x.A(x), b, left + right, Top, f(a), let x,y = A in B(x;y), x:A. B(x), Knd, Id, a:A fp B(a), x:AB(x), LocKnd, {x:A| B(x)} , t  T, x:A  B(x), let i,k:LocKnd = ik in P(i;k), Type
Lemmas	locknd-spread wf2, fpf-compose wf